M1, M2:msga{i:l}. ma-compatible{i:l}(M1; M2)  {i'} 

latex

Definitions

P  Q, x:A. B(x), x. t(x), Knd, Type, Id, f  g, Void, KindDeq, f  g, rcv(l,tg), IdDeq, t.2, Top, IdLnk, t.1, f(x)?z, type List, t  T, x.A(x), State(ds), x:AB(x), x:A  B(x), , , a:A fp B(a), P & Q, f || g, product-deq(A;B;a;b), IdLnkDeq, , A c B, Valtype(da;k), MsgA, M1 ||decl M2, M1 || M2

Lemmas

msga wf, Id wf, id-deq wf, Knd wf, Kind-deq wf, idlnk-deq wf, product-deq wf, fpf-compatible wf, fpf-trivial-subtype-top, IdLnk wf, subtype-fpf2, ma-state wf, bool wf, rationals wf, pi1 wf, top wf, fpf-join wf, rcv wf, pi2 wf, subtype rel product, subtype rel dep function, subtype rel self, subtype rel function, fpf-cap wf, subtype rel list, subtype-fpf-cap-top, subtype-fpf-cap-void, fpf-sub-join-left, fpf-sub-join-right